/*
 * Preprocessor.java
 * 
 * last update: 24.01.2010 by Olaru Victor
 * 
 * author:	Victor(victor.olaru@gmail.com)
 * 
 * Obs:
 */

package engine;
import java.util.*;

/**
 * This class is actually e helper for the preprocessing stuff, which
 * can be found inside VeriParser.jj
 */
final class Preprocessor
{
	/**
	 * This stack holds the the strems interrupted because of
	 * `included files.
	 */
	public static Stack<TokenMgrState> inStack;


	/**
	 * Here we push successful if(n)def's
	 * (the unsuccessful ones are treated immediately, by
	 * skippind to the closinf (`else/`endif) tag), so
	 * we can hadle their `else or `endif matching tags.
	 */
	private static Stack<Integer> ifdefStack;

	/**
	 * True when skipping parts from a file because
	 * `ifdef `ifndef. Whe set to true, all the preprocessing
	 * tags are simply ignored.
	 */
	public static boolean isSkipping;

	/**
	 * The ifdef level at which the skipping action startd.
	 */
	private static Stack<Integer> startLevel;

	/**
	 * Contains the `define'd macros.
	 */
	public static Hashtable<String, Macro> macrosHash;

	/**
	 * An estimation of the number of macros,
	 * based on the previous simulation.
	 */
	private static int macrosEstimate = 20;

	public static void init() {
		inStack = new Stack<TokenMgrState>();
		macrosHash = new Hashtable<String, Macro>(macrosEstimate);
		ifdefStack = new Stack<Integer>();
		startLevel = new Stack<Integer>();
		startLevel.push(new Integer(0));
	}

	public static final void performCleanup() {
		macrosEstimate = macrosHash.size();
		inStack = null;
		macrosHash = null;
	}

	////////////////////////////////
	// if(n)def STACKS HANDLING STUFF
	////////////////////////////////

	public static final void restoreStartLevel() {
		startLevel.pop();
	}

	public static final int newStartLevel(int l) {
		startLevel.push(new Integer(l));
		return l;
	}

	public static final int startLevel() {
		return ((Integer)startLevel.peek()).intValue();
	}

	public static final boolean  pushIfdef(boolean matched) {
		ifdefStack.push(new Integer(matched ? 1 : 0));
		return matched;
	}

	public static final boolean popIfdef() {
		return ((Integer) ifdefStack.pop()).intValue() != 0;
	}

	public static final boolean peekIfDef() {
		return ((Integer) ifdefStack.peek()).intValue() != 0;
	}

	public final static int ifdefLevel() {
		return ifdefStack.size();
	}

	public static final boolean isDefined(String name) {
		return macrosHash.get(name) != null;
	}

	///////////////////////
	// MACRO HANDLING STUFF
	///////////////////////

	public static final Macro getMacro(String name) {
		return (Macro) macrosHash.get(name);
	}

	public static final void undefine(String name) {
		macrosHash.remove(name);
	}

	public static void define(Macro m) {
		xConsole.tokenMgrTrace("defining \"" + m.name + "\" as \"" +
				m + "\"");
		macrosHash.put(m.name, m);
	}

	/////////////////////////
	// INCLUDE HANDLING STUFF
	/////////////////////////

	public static final void pushState(TokenMgrState s){
		inStack.push(s);
	}

	/**
	 * @exception EmptyStackException if no more streams
	 */
	public static final TokenMgrState popState() {
		return (TokenMgrState) inStack.pop();
	}

	public static final boolean moreIncludes() {
		return !inStack.empty();
	}
}

/**
 * This is used for saving/restoring the state of
 * the TokenManager.
 */
class TokenMgrState {
	String fileName;
	ASCII_CharStream in;

	TokenMgrState() {}

	TokenMgrState(String fileName, ASCII_CharStream in) {
		this.fileName = fileName;
		this.in = in;
	}

}

/**
 * A macro: its name, its expansion.
 */
class Macro {
	String name;

	/**
	 * Contains the elements that form the expansion of this macro
	 * it contains 1. Strings (the string parts between two occurenses of formal
	 * arguments); 2. Integers (the indexes of actual parameters that should be
	 * inserted at the current position.
	 */
	Object elements[];
	int paramNr;

	/**
	 * @param name the macro's name
	 * @param params a Vector of Strings (the names of the formal parameters)
	 * @param image the macro's image as defined on the `define line
	 */
	Macro(String name, Vector<String> params, String image) {
		if (xConsole.tokenManagerTrace) {
			String s = "`define \"" + name + "\"";
			if (params.size() > 0) {
				s += "(";
				for (int i = 0; i < params.size() ; i++)
					s += params.elementAt(i) + ", ";
				s += ")";
			}
			s += " as \"" + image;
			xConsole.tokenMgrTrace(s);
		}
		paramNr = params.size();
		Vector<String> elements  = new Vector<String>(1);
		this.name = name;
		elements.addElement(image);
		int paramNo = 0;
		for (Enumeration<String> p = params.elements(); p.hasMoreElements() ; paramNo++) {
			String pName = (String) p.nextElement();
			int pNameLen = pName.length();
			for (int elementIndex = 0; elementIndex < elements.size(); elementIndex++)
				try {
					String s = (String) elements.elementAt(elementIndex);
					int i, seen = 0;
					scanloop:
						while ((i = s.indexOf(pName, seen)) != -1) {
							if (i > 0) {
								if (isIdentifierPart(s.charAt(i-1))) {
									seen = i + 1;
									continue scanloop;
								}
								elements.setElementAt(s.substring(0, i), elementIndex++);
							}
							elements.insertElementAt(paramNo+"", elementIndex);
							int len = s.length();
							String s1 = s.substring(i + pNameLen, len);
							if (i < len - pNameLen) {
								if (isIdentifierPart(s.charAt(i-1))) {
									seen = i + len;
									continue scanloop;
								}
								elements.insertElementAt(s1, ++elementIndex);
							}
							s = s1;
						}
				} catch (ClassCastException cex) {}
		}
		this.elements = elements.toArray();
	}

	static final boolean isIdentifierPart(char c) {
		return (((c >= 'a') && (c <= 'z')) || ((c >= 'A') && (c <= 'Z')) ||
				((c >= '0') && (c <= '9')) || (c == '_'));
	}

	public String toString() {
		String s = "`define " + name + "  |";
		for (int i = 0; i < elements.length; i++)
			s += elements[i] + "|";
		return s;
	}

}






